Nuprl Lemma : nat_well_founded
9,38
postcript
pdf
WellFnd{i}(
;
x
,
y
.
x
<
y
)
latex
ProofTree
Definitions
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
t
T
,
{
T
}
,
x
(
s
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
Lemmas
nat
wf
,
comp
nat
ind
a
origin
;x,y.x < y)
;x,y.x < y)
T
Q
x:A. B(x)
x. t(x)